$\forall$${\it es}$:ES, ${\it ff}$:FIFO, $i$:${\it ff}$.C, $e$, ${\it e'}$:\{$e$:E$\mid$ ${\it ff}$.R($i$,$e$)\} , $j$:${\it ff}$.C.
\\[0ex](${\it ff}$.S($j$,$i$,${\it ff}$.Sender($i$,$e$)))
\\[0ex]$\Rightarrow$ (${\it ff}$.S($j$,$i$,${\it ff}$.Sender($i$,${\it e'}$)))
\\[0ex]$\Rightarrow$ ${\it ff}$.Sender($i$,$e$) c$\leq$ ${\it ff}$.Sender($i$,${\it e'}$)
\\[0ex]$\Rightarrow$ $e$ c$\leq$ ${\it e'}$